(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #x6A417BFA141EFFFF) #x6A417BFA141EFFFF))
(constraint (= (f #x9A19AA3639A1731C) #x9A19AA3639A1731D))
(constraint (= (f #xBB8F8177049D16BE) #xBB8F8177049D16BF))
(constraint (= (f #x34FB0E1CA10DD336) #x34FB0E1CA10DD337))
(constraint (= (f #x619D7D423C8D6401) #x619D7D423C8D6401))
(constraint (= (f #x7170BD10C7C4C2C4) #x7170BD10C7C4C2C5))
(constraint (= (f #x0C8D7659D8A6B63B) #x0C8D7659D8A6B63D))
(constraint (= (f #xA9084D35EA38F366) #xA9084D35EA38F367))
(constraint (= (f #xA2CD1BC056C66869) #xA2CD1BC056C6686B))
(constraint (= (f #x5BCA9932A21AB05D) #x5BCA9932A21AB05F))
(constraint (= (f #x00000000000FD846) #x00000000000FD846))
(constraint (= (f #x00000000000F5C06) #x00000000000F5C06))
(constraint (= (f #x00000000000EFFFF) #x00000000000EFFFF))
(constraint (= (f #x80000000000D0618) #x80000000000D0618))
(constraint (= (f #x00000000000D5F6B) #x00000000000D5F6B))
(constraint (= (f #x000000000000FFFF) #x0000000000010001))
(constraint (= (f #x800000000000FFFF) #x8000000000010001))
(constraint (= (f #x0000000000000002) #x0000000000000005))
(constraint (= (f #x8000000000000002) #x0000000000000005))
(constraint (= (f #x80000000000E5E1E) #x80000000000E5E1F))
(constraint (= (f #x800000000008970D) #x800000000008970F))
(constraint (= (f #x80000000000C27A0) #x80000000000C27A1))
(constraint (= (f #x80000000000C8238) #x80000000000C8239))
(constraint (= (f #x80000000000EC2B0) #x80000000000EC2B1))
(constraint (= (f #x800000000000F425) #x800000000000F427))
(constraint (= (f #x800000000000DAE1) #x800000000000DAE3))
(constraint (= (f #x800000000000A62F) #x800000000000A631))
(constraint (= (f #x000000000000CA62) #x000000000000CA63))
(constraint (= (f #x000000000000CB3A) #x000000000000CB3B))
(check-synth)
